Problem:
active(f(X,X)) -> mark(f(a(),b()))
active(b()) -> mark(a())
active(f(X1,X2)) -> f(active(X1),X2)
f(mark(X1),X2) -> mark(f(X1,X2))
proper(f(X1,X2)) -> f(proper(X1),proper(X2))
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2)) -> ok(f(X1,X2))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Proof:
Complexity Transformation Processor:
strict:
active(f(X,X)) -> mark(f(a(),b()))
active(b()) -> mark(a())
active(f(X1,X2)) -> f(active(X1),X2)
f(mark(X1),X2) -> mark(f(X1,X2))
proper(f(X1,X2)) -> f(proper(X1),proper(X2))
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2)) -> ok(f(X1,X2))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[top](x0) = x0 + 8,
[ok](x0) = x0 + 11,
[proper](x0) = x0 + 9,
[mark](x0) = x0 + 12,
[b] = 0,
[a] = 0,
[active](x0) = x0 + 10,
[f](x0, x1) = x0 + x1 + 4
orientation:
active(f(X,X)) = 2X + 14 >= 16 = mark(f(a(),b()))
active(b()) = 10 >= 12 = mark(a())
active(f(X1,X2)) = X1 + X2 + 14 >= X1 + X2 + 14 = f(active(X1),X2)
f(mark(X1),X2) = X1 + X2 + 16 >= X1 + X2 + 16 = mark(f(X1,X2))
proper(f(X1,X2)) = X1 + X2 + 13 >= X1 + X2 + 22 = f(proper(X1),proper(X2))
proper(a()) = 9 >= 11 = ok(a())
proper(b()) = 9 >= 11 = ok(b())
f(ok(X1),ok(X2)) = X1 + X2 + 26 >= X1 + X2 + 15 = ok(f(X1,X2))
top(mark(X)) = X + 20 >= X + 17 = top(proper(X))
top(ok(X)) = X + 19 >= X + 18 = top(active(X))
problem:
strict:
active(f(X,X)) -> mark(f(a(),b()))
active(b()) -> mark(a())
active(f(X1,X2)) -> f(active(X1),X2)
f(mark(X1),X2) -> mark(f(X1,X2))
proper(f(X1,X2)) -> f(proper(X1),proper(X2))
proper(a()) -> ok(a())
proper(b()) -> ok(b())
weak:
f(ok(X1),ok(X2)) -> ok(f(X1,X2))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[top](x0) = x0 + 11,
[ok](x0) = x0,
[proper](x0) = x0 + 5,
[mark](x0) = x0 + 5,
[b] = 8,
[a] = 8,
[active](x0) = x0,
[f](x0, x1) = x0 + x1
orientation:
active(f(X,X)) = 2X >= 21 = mark(f(a(),b()))
active(b()) = 8 >= 13 = mark(a())
active(f(X1,X2)) = X1 + X2 >= X1 + X2 = f(active(X1),X2)
f(mark(X1),X2) = X1 + X2 + 5 >= X1 + X2 + 5 = mark(f(X1,X2))
proper(f(X1,X2)) = X1 + X2 + 5 >= X1 + X2 + 10 = f(proper(X1),proper(X2))
proper(a()) = 13 >= 8 = ok(a())
proper(b()) = 13 >= 8 = ok(b())
f(ok(X1),ok(X2)) = X1 + X2 >= X1 + X2 = ok(f(X1,X2))
top(mark(X)) = X + 16 >= X + 16 = top(proper(X))
top(ok(X)) = X + 11 >= X + 11 = top(active(X))
problem:
strict:
active(f(X,X)) -> mark(f(a(),b()))
active(b()) -> mark(a())
active(f(X1,X2)) -> f(active(X1),X2)
f(mark(X1),X2) -> mark(f(X1,X2))
proper(f(X1,X2)) -> f(proper(X1),proper(X2))
weak:
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2)) -> ok(f(X1,X2))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[top](x0) = x0,
[ok](x0) = x0,
[proper](x0) = x0,
[mark](x0) = x0 + 8,
[b] = 10,
[a] = 0,
[active](x0) = x0,
[f](x0, x1) = x0 + x1 + 8
orientation:
active(f(X,X)) = 2X + 8 >= 26 = mark(f(a(),b()))
active(b()) = 10 >= 8 = mark(a())
active(f(X1,X2)) = X1 + X2 + 8 >= X1 + X2 + 8 = f(active(X1),X2)
f(mark(X1),X2) = X1 + X2 + 16 >= X1 + X2 + 16 = mark(f(X1,X2))
proper(f(X1,X2)) = X1 + X2 + 8 >= X1 + X2 + 8 = f(proper(X1),proper(X2))
proper(a()) = 0 >= 0 = ok(a())
proper(b()) = 10 >= 10 = ok(b())
f(ok(X1),ok(X2)) = X1 + X2 + 8 >= X1 + X2 + 8 = ok(f(X1,X2))
top(mark(X)) = X + 8 >= X = top(proper(X))
top(ok(X)) = X >= X = top(active(X))
problem:
strict:
active(f(X,X)) -> mark(f(a(),b()))
active(f(X1,X2)) -> f(active(X1),X2)
f(mark(X1),X2) -> mark(f(X1,X2))
proper(f(X1,X2)) -> f(proper(X1),proper(X2))
weak:
active(b()) -> mark(a())
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2)) -> ok(f(X1,X2))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Bounds Processor:
bound: 0
enrichment: match
automaton:
final states: {15,10,8,7,6,5}
transitions:
active0(15) -> 5*
active0(10) -> 5*
active0(2) -> 5*
active0(4) -> 5*
active0(1) -> 5*
active0(3) -> 5*
f0(3,1) -> 6*
f0(3,3) -> 6*
f0(3,15) -> 6*
f0(4,2) -> 6*
f0(4,4) -> 6*
f0(4,10) -> 6*
f0(15,1) -> 6*
f0(10,1) -> 6*
f0(15,3) -> 6*
f0(10,3) -> 6*
f0(15,15) -> 6*
f0(10,15) -> 6*
f0(1,2) -> 6*
f0(1,4) -> 6*
f0(1,10) -> 6*
f0(2,1) -> 6*
f0(2,3) -> 6*
f0(2,15) -> 6*
f0(3,2) -> 6*
f0(3,4) -> 6*
f0(3,10) -> 6*
f0(4,1) -> 6*
f0(4,3) -> 6*
f0(4,15) -> 6*
f0(15,2) -> 6*
f0(10,2) -> 6*
f0(15,4) -> 6*
f0(10,4) -> 6*
f0(15,10) -> 6*
f0(10,10) -> 6*
f0(1,1) -> 6*
f0(1,3) -> 6*
f0(1,15) -> 6*
f0(2,2) -> 6*
f0(2,4) -> 6*
f0(2,10) -> 6*
mark0(15) -> 1*
mark0(10) -> 1*
mark0(2) -> 10*,5,1
mark0(4) -> 1*
mark0(6) -> 6*
mark0(1) -> 1*
mark0(3) -> 1*
a0() -> 2*
b0() -> 3*
proper0(15) -> 7*
proper0(10) -> 7*
proper0(2) -> 7*
proper0(4) -> 7*
proper0(1) -> 7*
proper0(3) -> 7*
ok0(15) -> 4*
ok0(10) -> 4*
ok0(2) -> 15*,7,4
ok0(4) -> 4*
ok0(6) -> 6*
ok0(1) -> 4*
ok0(3) -> 15*,7,4
top0(15) -> 8*
top0(10) -> 8*
top0(5) -> 8*
top0(7) -> 8*
top0(2) -> 8*
top0(4) -> 8*
top0(1) -> 8*
top0(3) -> 8*
problem:
strict:
active(f(X1,X2)) -> f(active(X1),X2)
f(mark(X1),X2) -> mark(f(X1,X2))
proper(f(X1,X2)) -> f(proper(X1),proper(X2))
weak:
active(f(X,X)) -> mark(f(a(),b()))
active(b()) -> mark(a())
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2)) -> ok(f(X1,X2))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Bounds Processor:
bound: 0
enrichment: match
automaton:
final states: {13,10,8,7,6,5}
transitions:
active0(10) -> 5*
active0(2) -> 5*
active0(4) -> 5*
active0(1) -> 5*
active0(13) -> 5*
active0(3) -> 5*
f0(13,1) -> 6*
f0(13,3) -> 6*
f0(3,1) -> 6*
f0(3,3) -> 6*
f0(13,13) -> 6*
f0(3,13) -> 6*
f0(4,2) -> 6*
f0(4,4) -> 6*
f0(4,10) -> 6*
f0(10,1) -> 6*
f0(10,3) -> 6*
f0(10,13) -> 6*
f0(1,2) -> 6*
f0(1,4) -> 6*
f0(1,10) -> 6*
f0(2,1) -> 6*
f0(2,3) -> 6*
f0(2,13) -> 6*
f0(13,2) -> 6*
f0(13,4) -> 6*
f0(3,2) -> 6*
f0(3,4) -> 6*
f0(13,10) -> 6*
f0(3,10) -> 6*
f0(4,1) -> 6*
f0(4,3) -> 6*
f0(4,13) -> 6*
f0(10,2) -> 6*
f0(10,4) -> 6*
f0(10,10) -> 6*
f0(1,1) -> 6*
f0(1,3) -> 6*
f0(1,13) -> 6*
f0(2,2) -> 6*
f0(2,4) -> 6*
f0(2,10) -> 6*
mark0(10) -> 1*
mark0(2) -> 10*,5,1
mark0(4) -> 1*
mark0(6) -> 6*
mark0(1) -> 1*
mark0(13) -> 1*
mark0(3) -> 1*
a0() -> 2*
b0() -> 3*
proper0(10) -> 7*
proper0(2) -> 7*
proper0(4) -> 7*
proper0(1) -> 7*
proper0(13) -> 7*
proper0(3) -> 7*
ok0(10) -> 4*
ok0(2) -> 13*,7,4
ok0(4) -> 4*
ok0(6) -> 6*
ok0(1) -> 4*
ok0(13) -> 4*
ok0(3) -> 13*,7,4
top0(10) -> 8*
top0(5) -> 8*
top0(7) -> 8*
top0(2) -> 8*
top0(4) -> 8*
top0(1) -> 8*
top0(13) -> 8*
top0(3) -> 8*
problem:
strict:
f(mark(X1),X2) -> mark(f(X1,X2))
proper(f(X1,X2)) -> f(proper(X1),proper(X2))
weak:
active(f(X1,X2)) -> f(active(X1),X2)
active(f(X,X)) -> mark(f(a(),b()))
active(b()) -> mark(a())
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2)) -> ok(f(X1,X2))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Bounds Processor:
bound: 0
enrichment: match
automaton:
final states: {11,10,8,7,6,5}
transitions:
active0(10) -> 7*
active0(2) -> 7*
active0(4) -> 7*
active0(11) -> 7*
active0(1) -> 7*
active0(3) -> 7*
f0(3,1) -> 5*
f0(3,3) -> 5*
f0(3,11) -> 5*
f0(4,2) -> 5*
f0(4,4) -> 5*
f0(4,10) -> 5*
f0(10,1) -> 5*
f0(10,3) -> 5*
f0(10,11) -> 5*
f0(11,2) -> 5*
f0(11,4) -> 5*
f0(1,2) -> 5*
f0(1,4) -> 5*
f0(11,10) -> 5*
f0(1,10) -> 5*
f0(2,1) -> 5*
f0(2,3) -> 5*
f0(2,11) -> 5*
f0(3,2) -> 5*
f0(3,4) -> 5*
f0(3,10) -> 5*
f0(4,1) -> 5*
f0(4,3) -> 5*
f0(4,11) -> 5*
f0(10,2) -> 5*
f0(10,4) -> 5*
f0(10,10) -> 5*
f0(11,1) -> 5*
f0(11,3) -> 5*
f0(1,1) -> 5*
f0(1,3) -> 5*
f0(11,11) -> 5*
f0(1,11) -> 5*
f0(2,2) -> 5*
f0(2,4) -> 5*
f0(2,10) -> 5*
mark0(10) -> 1*
mark0(5) -> 5*
mark0(2) -> 10*,7,1
mark0(4) -> 1*
mark0(11) -> 1*
mark0(1) -> 1*
mark0(3) -> 1*
a0() -> 2*
b0() -> 3*
proper0(10) -> 6*
proper0(2) -> 6*
proper0(4) -> 6*
proper0(11) -> 6*
proper0(1) -> 6*
proper0(3) -> 6*
ok0(10) -> 4*
ok0(5) -> 5*
ok0(2) -> 11*,6,4
ok0(4) -> 4*
ok0(11) -> 4*
ok0(1) -> 4*
ok0(3) -> 11*,6,4
top0(10) -> 8*
top0(7) -> 8*
top0(2) -> 8*
top0(4) -> 8*
top0(11) -> 8*
top0(6) -> 8*
top0(1) -> 8*
top0(3) -> 8*
problem:
strict:
f(mark(X1),X2) -> mark(f(X1,X2))
weak:
proper(f(X1,X2)) -> f(proper(X1),proper(X2))
active(f(X1,X2)) -> f(active(X1),X2)
active(f(X,X)) -> mark(f(a(),b()))
active(b()) -> mark(a())
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2)) -> ok(f(X1,X2))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {15,14,12,8,7,6,5}
transitions:
active0(15) -> 7*
active0(2) -> 7*
active0(14) -> 7*
active0(4) -> 7*
active0(1) -> 7*
active0(3) -> 7*
f0(2,14) -> 5*
f0(3,1) -> 5*
f0(3,3) -> 5*
f0(3,15) -> 5*
f0(14,2) -> 5*
f0(14,4) -> 5*
f0(4,2) -> 5*
f0(4,4) -> 5*
f0(14,14) -> 5*
f0(4,14) -> 5*
f0(15,1) -> 5*
f0(15,3) -> 5*
f0(15,15) -> 5*
f0(1,2) -> 5*
f0(1,4) -> 5*
f0(1,14) -> 5*
f0(2,1) -> 5*
f0(2,3) -> 5*
f0(2,15) -> 5*
f0(3,2) -> 5*
f0(3,4) -> 5*
f0(3,14) -> 5*
f0(14,1) -> 5*
f0(14,3) -> 5*
f0(4,1) -> 5*
f0(4,3) -> 5*
f0(14,15) -> 5*
f0(4,15) -> 5*
f0(15,2) -> 5*
f0(15,4) -> 5*
f0(15,14) -> 5*
f0(1,1) -> 5*
f0(1,3) -> 5*
f0(1,15) -> 5*
f0(2,2) -> 5*
f0(2,4) -> 5*
mark0(15) -> 1*
mark0(2) -> 14*,7,1
mark0(14) -> 1*
mark0(4) -> 1*
mark0(1) -> 1*
mark0(3) -> 1*
a0() -> 2*
b0() -> 3*
proper0(15) -> 6*
proper0(2) -> 6*
proper0(14) -> 6*
proper0(4) -> 6*
proper0(1) -> 6*
proper0(3) -> 6*
ok0(15) -> 4*
ok0(5) -> 5*
ok0(12) -> 5*
ok0(2) -> 15*,6,4
ok0(14) -> 4*
ok0(4) -> 4*
ok0(1) -> 4*
ok0(3) -> 15*,6,4
top0(15) -> 8*
top0(7) -> 8*
top0(2) -> 8*
top0(14) -> 8*
top0(4) -> 8*
top0(6) -> 8*
top0(1) -> 8*
top0(3) -> 8*
mark1(10) -> 5*
mark1(5) -> 12*
mark1(12) -> 12*,5
f1(2,14) -> 5,12*
f1(3,1) -> 12*,5,10
f1(3,3) -> 12*,5,10
f1(3,15) -> 5,12*
f1(14,2) -> 5,12*
f1(14,4) -> 5,12*
f1(4,2) -> 12*,5,10
f1(4,4) -> 12*,5,10
f1(14,14) -> 5,12*
f1(4,14) -> 5,12*
f1(15,1) -> 5,12*
f1(15,3) -> 5,12*
f1(15,15) -> 5,12*
f1(1,2) -> 12*,5,10
f1(1,4) -> 12*,5,10
f1(1,14) -> 5,12*
f1(2,1) -> 12*,5,10
f1(2,3) -> 12*,5,10
f1(2,15) -> 5,12*
f1(3,2) -> 12*,5,10
f1(3,4) -> 12*,5,10
f1(3,14) -> 5,12*
f1(14,1) -> 5,12*
f1(14,3) -> 5,12*
f1(4,1) -> 12*,5,10
f1(4,3) -> 12*,5,10
f1(14,15) -> 5,12*
f1(4,15) -> 5,12*
f1(15,2) -> 5,12*
f1(15,4) -> 5,12*
f1(15,14) -> 5,12*
f1(1,1) -> 12*,5,10
f1(1,3) -> 12*,5,10
f1(1,15) -> 5,12*
f1(2,2) -> 12*,5,10
f1(2,4) -> 12*,5,10
ok1(5) -> 5,12*
ok1(12) -> 5,12*
problem:
strict:
weak:
f(mark(X1),X2) -> mark(f(X1,X2))
proper(f(X1,X2)) -> f(proper(X1),proper(X2))
active(f(X1,X2)) -> f(active(X1),X2)
active(f(X,X)) -> mark(f(a(),b()))
active(b()) -> mark(a())
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2)) -> ok(f(X1,X2))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Qed